Goto

Collaborating Authors

 proof planning exhibit


Meier

AAAI Conferences

Proof planning considers mathematical theorem proving as a planning problem. It has enabled the derivation of mathematical theorems that lay outside the scope of traditional logic-based theorem proving systems. One of its strengths comes from heuristic mathematical knowledge that restricts the search space and thereby facilitates the proving process for problems whose proofs belong in the restricted search space. But this may exclude solutions or restrict the kinds of proofs that can be found for a given problem. We take a different perspective and investigate problem classes for which little or no heuristic control knowledge is available and test the usage of randomization and restart techniques.